Cancel(T;S;op) ==
u, v:T, w:S. ((w op u) = (w op v)) 
(u = v)
clarification:
basic
Cancel(T;S;op) ==
u:T, v:T, w:S. ((w op u) = (w op v) 
T) (u = v T) | 13,42 |
u, v:T, w:S. ((w op u) = (w op v)) (u = v)
u:T, v:T, w:S. ((w op u) = (w op v) T) (u = v T)
| Up | |
| Wellformedness Lemmas | |
| Definitions | x:A. B(x) Q |